--Submitted by
-- Dhasarathy Parthasarathy
-- Anandhavel Sakthivel
-- Changes in response to Mary's comments are marked with ##
-- functions for running all the test cases at the end of the file. Done our best to exclude time consuming test cases in this full run
import Lava
import Lava.Patterns
import Lava.Arithmetic

type Bit = Signal Bool
type Binary = [Bit]

-- ## Test cases for every problem Ai are functions of name testAixj
--Every testcase testAixj has been run and the outputs have been verified. The generated outputs confirm the correctness of the descriptions
--A1
binAdder1 :: (Binary,Binary) -> Binary
binAdder1 (a:as, b:bs) = [s] ++ sum ++ [carryOut]
	where
    (sum,carryOut) = adder(c0,(as,bs));
	(s,c0) = halfAdd(a,b);

--verification
add2 :: (Signal Int,Signal Int) -> Signal Int	
add2 (a,b) = a + b 

-- to produce n bit pairs test vectors and reference integers
-- ## listOfPairOfBinaries is derived from listOfPairOfIntegers
listOfPairOfBinaries n = [ ((int2bin n x),(int2bin n y)) | (x,y)<-(listOfPairOfIntegers n)]
listOfPairOfIntegers n = ([ (x,y) | x<-[0..m],y<-[0..m]])
	where
	m = fromInteger (2^n-1)

--checks equality of an n bit adder output with the '+' operation for equal length inputs case
binAdder1Test n = ok 
	where
	adderBinaryOutput = simulateSeq binAdder1 (listOfPairOfBinaries n)
	adderIntegerOutput = simulateSeq bin2int(adderBinaryOutput)
	referenceIntegerOutput = simulateSeq add2 (listOfPairOfIntegers n)
	ok = adderIntegerOutput <==> referenceIntegerOutput

-- ## testing binAdder1 for input binaries of the same length	
testA1x0 = simulate binAdder1Test 2
testA1x1 = simulate binAdder1Test 3
testA1x2 = simulate binAdder1Test 4
testA1x3 = simulate binAdder1Test 5

exhaustiveTestBinAdder1 = [testA1x0,testA1x1,testA1x2,testA1x3]

-- to produce m and n bit pairs test vectors and reference integers
listOfPairOfBinariesDiffLen m n = [ ((int2bin m x),(int2bin n y)) | (x,y)<-(listOfPairOfIntegersDiffLen m n)]
listOfPairOfIntegersDiffLen m n = ([ (x,y) | x<-[0..p],y<-[0..q]])
	where
	p = fromInteger (2^m-1)
	q = fromInteger (2^n-1)

-- ## test function for inputs of different length
binAdder1TestDiffLen m n = ok
	where
	adderBinaryOutput = simulateSeq binAdder1 (listOfPairOfBinariesDiffLen m n)
	adderIntegerOutput = simulateSeq bin2int(adderBinaryOutput)
	referenceIntegerOutput = simulateSeq add2 (listOfPairOfIntegersDiffLen m n)
	ok = simulate id (adderIntegerOutput <==> referenceIntegerOutput)

-- ## testing binAdder1 for input binaries of different lengths for unequal length inputs case
testA1x4 = binAdder1TestDiffLen 2 3
testA1x5 = binAdder1TestDiffLen 3 4
testA1x6 = binAdder1TestDiffLen 4 5

exhaustiveTestBinAdder1DiffLen = [testA1x4,testA1x5,testA1x6]
-------------------------------------------------------------------------------------------------------------------------------------------------------------
--A2
-- linear array of 2 i/p 1 o/p circuits
linearArray circ (cIn,[]) = (cIn)
linearArray circ (cIn,a:as) = (cOut)
	where
	cNext = circ (cIn,a)
	cOut = linearArray circ (cNext,as)

-- suggested test in lab questions	
testA2x0 = simulate (linearArray plus) (0,[1..7])
-------------------------------------------------------------------------------------------------------------------------------------------------------------
--A3
number cs = zip cs [0..length cs - 1]

-- to perform Bit*Binary multiplication
vectorMult :: (Bit,Binary) -> Binary
vectorMult (a,bs) = [and2(a,x) | x<-bs]

-- produces padded partial products
shiftPartMult :: (Bit,Binary,Int) -> Binary
shiftPartMult (a,bs,m) = ds
	where
	dx = vectorMult(a,bs) 
	ds =  (replicate m low) ++ dx
	
prods_as_bin :: (Binary,Binary) -> [Binary]	
prods_as_bin (as,bs) = [ shiftPartMult (a,bs,m) | (a,m) <- number as]
-------------------------------------------------------------------------------------------------------------------------------------------------------------
--A4
-- adds padded partial products using a linearArray of binAdder1s
binMultiplier :: (Binary,Binary) -> Binary
binMultiplier (as,bs) = cs
	where
	cs = (linearArray binAdder1)((replicate (length bs) low),prods_as_bin (as,bs))
-------------------------------------------------------------------------------------------------------------------------------------------------------------
--A5
-- to equalize 2 lists using padding because of extra carry out from the binary adder
equalizeLength2 :: (Binary,Binary) -> (Binary,Binary)
equalizeLength2 (a,b) = (x,y)
	where
	maxLength = maximum [(length a),(length b)]
	equalLength = (length a) == (length b) -- ## Function common for several multipliers so conditional padding done
	(x,y) = if equalLength
		then (a,b)
		else ((a ++ replicate (maxLength - (length a)) low),(b ++ replicate (maxLength - (length b)) low))

-- exhaustive test	
mult2 :: (Signal Int,Signal Int) -> Signal Int	
mult2 (a,b) = a * b 	

binMultiplierTest n = ok --checks equality of an n bit adder output with the '*' operation
	where
	multiplierBinaryOutput = simulateSeq binMultiplier (listOfPairOfBinaries n)
	multiplierIntegerOutput = simulateSeq bin2int(multiplierBinaryOutput)
	referenceMultIntegerOutput = simulateSeq mult2 (listOfPairOfIntegers n)
	ok = multiplierIntegerOutput <==> referenceMultIntegerOutput
	
testA5x0 = simulate binMultiplierTest 2
testA5x1 = simulate binMultiplierTest 3
testA5x2 = simulate binMultiplierTest 4
--testA5x3 = simulate binMultiplierTest 5	--takes too much time but gives high

exhaustiveTestBinMultiplier = [testA5x0,testA5x1,testA5x2] 							

-- formal verification 
-- generalized check of two lists after equalizing length by padding
propEquivalenceCheck circ1 circ2 a = ok
	where
	out1 = circ1 a
	out2 = circ2 a
	(x,y) = equalizeLength2(out1,out2)
	ok = x <==> y

-- setting bounds
propEquivalenceCheckForSizeN n a b = forAll (list n) $ \as -> forAll (list n) $ \bs -> propEquivalenceCheck a b (as,bs)

-- SMV and SAT tests using multi as the 'golden' reference model
testA5x5 = smv (propEquivalenceCheckForSizeN 2 binMultiplier multi)
testA5x6 = smv (propEquivalenceCheckForSizeN 4 binMultiplier multi)
testA5x7 = smv (propEquivalenceCheckForSizeN 6 binMultiplier multi)
testA5x8 = smv (propEquivalenceCheckForSizeN 8 binMultiplier multi)
testA5x9 = satzoo (propEquivalenceCheckForSizeN 2 binMultiplier multi)
testA5x10 = satzoo (propEquivalenceCheckForSizeN 4 binMultiplier multi)
testA5x11 = satzoo (propEquivalenceCheckForSizeN 6 binMultiplier multi)
testA5x12 = satzoo (propEquivalenceCheckForSizeN 8 binMultiplier multi)

formalVerBinMultiplierSMV = do 
						testA5x5 
						testA5x6 
						testA5x7 
						testA5x8
						
formalVerBinMultiplierSAT = do						
						testA5x9
						testA5x10
						testA5x11
						testA5x12
-------------------------------------------------------------------------------------------------------------------------------------------------------------						
--A6
binAdder2 :: (Binary,Binary) -> (Bit,Binary)
binAdder2 (a:as, b:bs) = (s,sum ++ [carryOut])
	where
    (sum,carryOut) = adder(c0,(as,bs));
	(s,c0) = halfAdd(a,b);

shiftPartMult2 :: (Bit,Binary) -> Binary
shiftPartMult2 (a,bs) = vectorMult (a,bs)

partProducts :: (Binary,Binary) -> [Binary] -- no padding to the partial products
partProducts (as,bs) = [ shiftPartMult2 (a,bs) | a<-as]

linearArray2x2 circ(cIn,[]) = ([],cIn) -- linear array of 2 i/p 2 o/p circuits
linearArray2x2 circ(cIn,a:as) = (b:bs,cOut)
	where
	(b,cNext) = circ (cIn,a)
	(bs,cOut) = linearArray2x2 circ (cNext,as)

binMultiplier1 :: (Binary,Binary) -> Binary
binMultiplier1 (as,bs) = cs++ds
	where
	(cs,ds) = (linearArray2x2 binAdder2) ((replicate (length bs) low),partProducts (as,bs));

--verification
testA6x0 = smv (propEquivalenceCheckForSizeN 2 binMultiplier1 multi)
testA6x1 = smv (propEquivalenceCheckForSizeN 4 binMultiplier1 multi)
testA6x2 = smv (propEquivalenceCheckForSizeN 6 binMultiplier1 multi)
testA6x3 = smv (propEquivalenceCheckForSizeN 8 binMultiplier1 multi)
testA6x4 = satzoo (propEquivalenceCheckForSizeN 2 binMultiplier1 multi)
testA6x5 = satzoo (propEquivalenceCheckForSizeN 4 binMultiplier1 multi)
testA6x6 = satzoo (propEquivalenceCheckForSizeN 6 binMultiplier1 multi)
testA6x7 = satzoo (propEquivalenceCheckForSizeN 8 binMultiplier1 multi)


formalVerBinMultiplier1SMV = do 
						testA6x0 
						testA6x1 
						testA6x2 
						testA6x3

formalVerBinMultiplier1SAT = do						
						testA6x4
						testA6x5
						testA6x6
						testA6x7
-------------------------------------------------------------------------------------------------------------------------------------------------------------						
--A7
-- full adder for 3:2 compression
halfAdder :: (Bit,Bit) -> (Bit,Bit)
halfAdder (a, b) = (sum, carry)
  where
    sum   = xor2 (a, b)
    carry = and2 (a, b)

fullAdder :: (Bit,Bit,Bit) -> (Bit,Bit)
fullAdder (carryIn, a, b) = (sum, carryOut)
  where
    (s1,  c1) = halfAdder (a, b)
    (sum, c2) = halfAdder (carryIn, s1)
    carryOut  = xor2 (c2, c1)

-- map of 3 i/p 2o/p circuits	
map3x2 f ([],[],[]) = ([],[])
map3x2 f (a:as,b:bs,c:cs) = (d:ds,e:es)
	where
	(d,e) = f(a,b,c);
	(ds,es) = map3x2 f (as,bs,cs)

-- length equalizer for 3 lists
equalizeLength :: (Binary,Binary,Binary) -> (Binary,Binary,Binary) -- for padding shorter lists
equalizeLength (a,b,c) = (x,y,z)
	where
	maxLength = maximum [(length a),(length b),(length c)]
	x =  a ++ replicate (maxLength - (length a)) low
	y =  b ++ replicate (maxLength - (length b)) low
	z =  c ++ replicate (maxLength - (length c)) low	

type CsvBinary = [(Bit,Bit)]

-- ## CSV consideration -> carry bits have one weight extra so a 0 is padded at LSB to the carry vector before processing
-- LSB padding for the binary number bIn is not done here as the prods_as_bin which generates the partial products already pads them
-- 3:2 compression using full adders
csvAdder :: (CsvBinary,Binary) -> CsvBinary
csvAdder (csvIn,bIn) = zipp(sOut,cOut)
	where
	(sIn,cIn) = unzipp(csvIn)
	(x,y,z) = equalizeLength (sIn,[low] ++ cIn,bIn)
	(sOut,cOut) = (map3x2 fullAdder) (x,y,z)

-- ## linearArray csvAdder now replaces the recursive call	
-- cascade of csvAdder
cascededCsvAdder :: [Binary] -> CsvBinary
cascededCsvAdder (a:as) = bs
	where
	bs = (linearArray csvAdder) ((replicate ((length a)-1) (low,low)),a:as)

-- partial products generated for addition and final csv to binary form conversion for formal verification as a multiplier
cascadedCsvMultiplier :: (Binary,Binary) -> Binary
cascadedCsvMultiplier ([],[]) = []
cascadedCsvMultiplier (a,b) = c
	where
	xs = prods_as_bin (a,b)
	csvPdt = cascededCsvAdder xs
	(m,n) = unzipp(csvPdt)
	c = binAdder1(m ++ [low],[low] ++ n)

--verification
testA7x0 = smv (propEquivalenceCheckForSizeN 2 cascadedCsvMultiplier multi)
testA7x1 = smv (propEquivalenceCheckForSizeN 4 cascadedCsvMultiplier multi)
testA7x2 = smv (propEquivalenceCheckForSizeN 6 cascadedCsvMultiplier multi)
testA7x3 = smv (propEquivalenceCheckForSizeN 8 cascadedCsvMultiplier multi)
testA7x4 = satzoo (propEquivalenceCheckForSizeN 2 cascadedCsvMultiplier multi)
testA7x5 = satzoo (propEquivalenceCheckForSizeN 4 cascadedCsvMultiplier multi)
testA7x6 = satzoo (propEquivalenceCheckForSizeN 6 cascadedCsvMultiplier multi)
testA7x7 = satzoo (propEquivalenceCheckForSizeN 8 cascadedCsvMultiplier multi)

formalVercascadedCsvMultiplierSMV = do
									testA7x0
									testA7x1
									testA7x2
									testA7x3
									
formalVercascadedCsvMultiplierSAT = do
									testA7x4
									testA7x5
									testA7x6
									testA7x7									
-------------------------------------------------------------------------------------------------------------------------------------------------------------
--A8
-- binary tree of circuits
binTree circ [inp] = inp
binTree circ inps = (halveList ->-(binTree circ -|- binTree circ) ->- circ) inps

-- binary tree of binAdder1
binAdder3 :: (Binary,Binary) -> Binary
binAdder3 (as,bs) = sum ++ [carryOut]
	where
	(sum,carryOut) = adder(low,(as,bs))

treeAdder :: ([Binary]) -> Binary
treeAdder (as) = (binTree binAdder1) as

-- partial product generation and feeding them to the binary tree of binAdder1
binMultiplier3 :: (Binary,Binary) -> Binary
binMultiplier3 (as,bs) = cs
	where
	cs = treeAdder (prods_as_bin (as,bs));

--verification	
testA8x0 = smv (propEquivalenceCheckForSizeN 2 binMultiplier3 multi)
testA8x1 = smv (propEquivalenceCheckForSizeN 4 binMultiplier3 multi)
testA8x2 = smv (propEquivalenceCheckForSizeN 6 binMultiplier3 multi)
testA8x3 = smv (propEquivalenceCheckForSizeN 8 binMultiplier3 multi)
testA8x4 = satzoo (propEquivalenceCheckForSizeN 2 binMultiplier3 multi)
testA8x5 = satzoo (propEquivalenceCheckForSizeN 4 binMultiplier3 multi)
testA8x6 = satzoo (propEquivalenceCheckForSizeN 6 binMultiplier3 multi)
testA8x7 = satzoo (propEquivalenceCheckForSizeN 8 binMultiplier3 multi)

formalVerBinMultiplier3SMV = do 
						testA8x0 
						testA8x1 
						testA8x2 
						testA8x3
						
formalVerBinMultiplier3SAT = do 						
						testA8x4
						testA8x5
						testA8x6
						testA8x7
-------------------------------------------------------------------------------------------------------------------------------------------------------------
--A9	
-- map of 3 input circuits
gmap3 f []  = []
gmap3 f [a] = [a]
gmap3 f [a,b] = [a,b]
gmap3 f (a:b:c:ds) = f (a,b,c) ++ gmap3 f ds

-- map of full adders for carry-save addition		
csvAdder2 :: (Binary,Binary,Binary) -> [Binary]
csvAdder2 (a,b,c) = [d ++ [low],[low] ++ e]
	where
	(x,y,z) = equalizeLength (a,b,c)
	(d,e) = (map3x2 fullAdder) (x,y,z)

-- tree of carry save adders	
wallaceTree :: [Binary] -> [Binary]
wallaceTree [a]   = [a]
wallaceTree [a,b] = [a,b]
wallaceTree as = cs
	where
	cNexts = (gmap3 csvAdder2) as
	cs = wallaceTree cNexts

-- parial products generated for addition and final conversion of the carry save form to binary for for verification as a multiplier	
wallaceTreeMultiplier :: (Binary,Binary) -> Binary
wallaceTreeMultiplier (as,bs) = binAdder1(cs,ds)
	where
	[cs,ds] = wallaceTree (prods_as_bin (as,bs))

--verification	
testA9x0 = smv (propEquivalenceCheckForSizeN 2 wallaceTreeMultiplier multi)
testA9x1 = smv (propEquivalenceCheckForSizeN 4 wallaceTreeMultiplier multi)
testA9x2 = smv (propEquivalenceCheckForSizeN 6 wallaceTreeMultiplier multi)
testA9x3 = smv (propEquivalenceCheckForSizeN 8 wallaceTreeMultiplier multi)
testA9x4 = satzoo (propEquivalenceCheckForSizeN 2 wallaceTreeMultiplier multi)
testA9x5 = satzoo (propEquivalenceCheckForSizeN 4 wallaceTreeMultiplier multi)
testA9x6 = satzoo (propEquivalenceCheckForSizeN 6 wallaceTreeMultiplier multi)
testA9x7 = satzoo (propEquivalenceCheckForSizeN 8 wallaceTreeMultiplier multi)

formalVerwallaceTreeMultiplierSMV = do 
								testA9x0 
								testA9x1 
								testA9x2 
								testA9x3

formalVerwallaceTreeMultiplierSAT = do 								
								testA9x4
								testA9x5
								testA9x6
								testA9x7
-------------------------------------------------------------------------------------------------------------------------------------------------------------
-- functions for running all the tests								
allExhaustiveTests = do
					 exhaustiveTestBinAdder1
					 exhaustiveTestBinMultiplier
					
allSMVTests = do
			  formalVerBinMultiplierSMV
			  formalVerBinMultiplier1SMV
			  formalVercascadedCsvMultiplierSMV
			  formalVerBinMultiplier3SMV
			  formalVerwallaceTreeMultiplierSMV

allSATTests = do			  
			  formalVerBinMultiplierSAT
			  formalVerBinMultiplier1SAT
			  formalVercascadedCsvMultiplierSAT
			  formalVerBinMultiplier3SAT
			  formalVerwallaceTreeMultiplierSAT